﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

using SimpleIR;
using RgnAnalyzer.Domain;

namespace RgnAnalyzer
{
	/// <summary>
	/// Each call context needs to keep track of the current internal evaluation state.
	/// This way we can freeze and resume it whenever we want to.
	/// </summary>
	internal sealed class MethodEvalState
	{
		/// <summary>
		/// A stack of regions (and a per region interp of a position in the location of processing in this region).
		/// </summary>
		private readonly LinkedList<T1T2RegionEvalState> m_rgnsAnalyzedAndPos;

		/// <summary>
		/// A map from (endblock, startblock) id pairs for edges, to the flow state on said edge (or if bottom then the value is not in the map).
		/// </summary>
		private readonly Dictionary<long, Dictionary<long, AProgramMemory>> m_flowEdgeToStateMap;

		/// <summary>
		/// If we freeze for a pending call this is the model to use when restarting the analysis of the call statment.
		/// </summary>
		private AProgramMemory m_pendingCallModelForRestart;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_rgnsAnalyzedAndPos != null);
			Contract.Invariant(this.m_flowEdgeToStateMap != null);
		}

		internal MethodEvalState()
		{
			this.m_rgnsAnalyzedAndPos = new LinkedList<T1T2RegionEvalState>();
			this.m_flowEdgeToStateMap = new Dictionary<long, Dictionary<long, AProgramMemory>>();
		}

		////////////////////////////////////////
		//setup/teardown and access the intermediate analysis state info

		internal void ResetAnalysisInformation()
		{
			this.m_rgnsAnalyzedAndPos.Clear();
			this.m_flowEdgeToStateMap.Clear();
		}

		/// <summary>
		/// Set the given flow value for the edge between the specified blocks.
		/// </summary>
		internal void SetFlowEdgeModel(long startblock, long trgtblock, AProgramMemory m)
		{
			if(m == null)
				return;
			
			if(!this.m_flowEdgeToStateMap.ContainsKey(trgtblock))
				this.m_flowEdgeToStateMap.Add(trgtblock, new Dictionary<long, AProgramMemory>());

			Dictionary<long, AProgramMemory> npm = this.m_flowEdgeToStateMap[trgtblock];
			if(!npm.ContainsKey(startblock))
				npm.Add(startblock, m);
			else
				npm[startblock] = m;
		}

		/// <summary>
		/// At the exit of loops that do traversals we use this to nuke any traversal info that may 
		/// appear at the flow exits of the loop.
		/// </summary>
		internal void UpdateFlowLocationsAndClearLoopTraversalInfoOnLoopExit(T1T2LoopEvalState ll)
		{
			HashSet<long> allblocks = new HashSet<long>();
			allblocks.Add(ll.T1T2Loop.Head.BlockID);
			allblocks.UnionWith(ll.T1T2Loop.AllContainedBlocks);
			int loopmin = ll.T1T2Loop.MinStmt();
			int loopmax = ll.T1T2Loop.MaxStmt();

			foreach(Dictionary<long, AProgramMemory> npm in this.m_flowEdgeToStateMap.Values)
			{
				foreach(long startblockid in allblocks)
				{
					if(npm.ContainsKey(startblockid))
					{
						npm[startblockid].AdvanceUseModAndAllocInfoToLoopPrevious(loopmin, loopmax, ll.T1T2Loop.LoopLastIterUseModLoc);
						if(ll.T1T2Loop.DoLoopTraverseOperations)
							npm[startblockid].ClearLoopPositionInfo();
					}
				}
			}
		}

		/// <summary>
		/// Get a dictionary mapping from source blockids to sets of models incomming from these blocks (this clears the corresponding values from the flow edges).
		/// </summary>
		internal void FetchAllIncommingFlowEdgeModels(long trgtblock, List<AProgramMemory> allinmodels)
		{
			Contract.Requires(allinmodels != null && allinmodels.Count == 0);
			
			if(this.m_flowEdgeToStateMap.ContainsKey(trgtblock))
			{
				allinmodels.AddRange(this.m_flowEdgeToStateMap[trgtblock].Values);
				this.m_flowEdgeToStateMap.Remove(trgtblock);
			}
		}

		////////////////////////////////////////
		//get various componenents

		/// <summary>
		/// Return true if there is no more work to be done in the local analysis.
		/// </summary>
		internal bool LocalAnalysisComplete
		{ get { return this.m_rgnsAnalyzedAndPos.Count == 0; } }
			
		/// <summary>
		/// Get the eval state for the region that is currently being analyzed.
		/// </summary>
		internal T1T2RegionEvalState CurrentT1T2EvalRegion
		{
			get
			{
				Contract.Ensures(Contract.Result<T1T2RegionEvalState>() != null);

				return this.m_rgnsAnalyzedAndPos.Last();
			}
		}

		/// <summary>
		/// Push the given basic block on the stack of regions that we need to analyze.
		/// </summary>
		internal void PushBasicBlockForAnalysis(IRBasicBlock bb)
		{
			this.m_rgnsAnalyzedAndPos.AddLast(new T1T2BasicBlockEvalState(bb));
		}

		/// <summary>
		/// Push the given region on the stack of regions that we need to analyze.
		/// </summary>
		internal void PushT1T2RegionForAnalysis(IRT1T2Region rgn)
		{
			Contract.Requires(rgn != null && ((rgn is IRT1T2Block) | (rgn is IRT1T2Loop)));

			if(rgn is IRT1T2Block)
				this.m_rgnsAnalyzedAndPos.AddLast(new T1T2BlockEvalState((IRT1T2Block)rgn));
			else
				this.m_rgnsAnalyzedAndPos.AddLast(new T1T2LoopEvalState((IRT1T2Loop)rgn));
		}

		/// <summary>
		/// Pop the most recent region off the stack of T1T2Regions we need to analyze.
		/// </summary>
		internal void PopCompletedT1T2Region()
		{
			this.m_rgnsAnalyzedAndPos.RemoveLast(); 
		}

		/// <summary>
		/// Get the outermost currently active loop that is being analyzed.
		/// </summary>
		internal IRT1T2Loop GetCurrentOutermostLoop()
		{
			LinkedListNode<T1T2RegionEvalState> lln = this.m_rgnsAnalyzedAndPos.First;
			while(!(lln.Value is T1T2LoopEvalState))
				lln = lln.Next;

			return ((T1T2LoopEvalState)lln.Value).T1T2Loop;
		}

		/// <summary>
		/// Get the model that is the state to resume with if we are frozen during a call analysis
		/// </summary>
		internal AProgramMemory FrozenCallResumeModel
		{
			get { return this.m_pendingCallModelForRestart; }
			set { this.m_pendingCallModelForRestart = value; }
		}

		//////////////////////////////////////////////////////////////
		//Analysis Flow Output

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintEvalLoopFrozenForCall(DebugState dbgs)
		{
			if(dbgs == DebugState.DebugStep)
				Console.WriteLine("      Local Eval Frozen For Call.");
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintEvalLoopPopCompleteComponent(DebugState dbgs)
		{
			if(dbgs == DebugState.DebugStep)
				Console.WriteLine("      Return From Eval Pop From Stack.");
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal static void Display__PrintEvalLoopReturnForEvalOfPush(DebugState dbgs)
		{
			if(dbgs == DebugState.DebugStep)
				Console.WriteLine("      Return For Eval of Sub-Component.");
		}

		[System.Diagnostics.Conditional("DEBUG_ENABLED")]
		internal void Display__PrintPendingStateList()
		{
			StringBuilder sb = new StringBuilder("      PendingLocal:");
			sb.Append("\n      [\n");

			bool first = true;
			foreach(T1T2RegionEvalState rrs in this.m_rgnsAnalyzedAndPos)
			{
				if(!first)
					sb.Append(", \n");
				first = false;

				sb.Append("        " + LocalAnalysisContextForStatus(rrs));
			}
			sb.Append("\n      ]");

			Console.WriteLine(sb.ToString());
		}

		private static String LocalAnalysisContextForStatus(T1T2RegionEvalState rrs)
		{
			if(rrs is T1T2LoopEvalState)
			{
				T1T2LoopEvalState lls = (T1T2LoopEvalState)rrs;
				return "(Loop " + lls.T1T2Loop.Head.BlockID + ": " + lls.CurrentlyAnalysisResumeState + ")";
			}
			else if(rrs is T1T2BlockEvalState)
			{
				T1T2BlockEvalState bbs = (T1T2BlockEvalState)rrs;
				String pos = (bbs.T1T2Block.T1T2Blocks[0] is IRBasicBlock) ? ("Blck-" + ((IRBasicBlock)bbs.T1T2Block.T1T2Blocks[0]).BlockID) : ("Loop-" + ((IRT1T2Loop)bbs.T1T2Block.T1T2Blocks[0]).Head.BlockID);
				return "(DagOfBlocks " + pos + ": " + bbs.CurrentSubRegionIndex + "of" + bbs.T1T2Block.T1T2Blocks.Count + ")";
			}
			else
			{
				T1T2BasicBlockEvalState bbes = (T1T2BasicBlockEvalState)rrs;
				return "(BasicBlock " + bbes.BasicBlock.BlockID + ": " + bbes.CurrentSubRegionIndex + ")";
			}
		}
	}

	/// <summary>
	/// Keep track of the state of analyzing a T1T2Region
	/// </summary>
	internal abstract class T1T2RegionEvalState
	{
		/// <summary>
		/// The region that we are in.
		/// </summary>
		protected readonly IRT1T2Region m_rgn;

		[ContractInvariantMethod]
		private void ObjectInvariant()
		{
			Contract.Invariant(this.m_rgn != null);
		}

		protected T1T2RegionEvalState(IRT1T2Region rgn)
		{
			Contract.Requires(rgn != null);

			this.m_rgn = rgn; 
		}
	}

	/// <summary>
	/// Keep track of the state of analyzing a T1T2Region
	/// </summary>
	internal sealed class T1T2LoopEvalState : T1T2RegionEvalState
	{
		internal enum LoopResumeState { InitializeLoopInit, ResumeAtTest, ResumeInHead, ResumeInBody, ResumeInPostLoopJoin };

		/// <summary>
		/// The point at which we want to resume the analysis of this loop.
		/// </summary>
		private LoopResumeState m_resumeState;

		/// <summary>
		/// The <c>PModel</c> value generated for the last iteration of the fixpoint approximation.
		/// </summary>
		private AProgramMemory m_lastLoopModel;

		/// <summary>
		/// The <c>PModel</c> value generated for the current iteration of the fixpoint approximation.
		/// </summary>
		private AProgramMemory m_currentLoopModel;

		/// <summary>
		/// The <c>PModel</c> value generated by the initial inputs to the loop.
		/// </summary>
		private AProgramMemory m_origEntryLoopModel;

		/// <summary>
		/// The number of iterations in the fixpoint computation we have done so far.
		/// </summary>
		public int LoopIterCtr;

		internal T1T2LoopEvalState(IRT1T2Loop loop)
			: base(loop)
		{
			Contract.Requires(loop != null);

			this.m_resumeState = LoopResumeState.InitializeLoopInit;
			this.m_lastLoopModel = null;
			this.m_origEntryLoopModel = null;
			this.LoopIterCtr = 0;
		}

		/// <summary>
		/// Get/Set if we are currently analyzing the head or the body (if it exists) of the loop.
		/// </summary>
		internal LoopResumeState CurrentlyAnalysisResumeState
		{
			get { return this.m_resumeState; }
			set { this.m_resumeState = value; }
		}

		/// <summary>
		/// Get/Set the last model state for the loop fixpoint approximation.
		/// </summary>
		internal AProgramMemory LastPModelApprox
		{
			get { return this.m_lastLoopModel; }
			set { this.m_lastLoopModel = value; }
		}

		/// <summary>
		/// Get/Set the current model state for the loop fixpoint approximation.
		/// </summary>
		internal AProgramMemory CurrentPModelApprox
		{
			get { return this.m_currentLoopModel; }
			set { this.m_currentLoopModel = value; }
		}

		/// <summary>
		/// Get/Set the last model state for the loop fixpoint approximation.
		/// </summary>
		internal AProgramMemory OrigLoopEntryPModelApprox
		{
			get { return this.m_origEntryLoopModel; }
			set { this.m_origEntryLoopModel = value; }
		}

		/// <summary>
		/// Get the loop that this eval state relates to.
		/// </summary>
		internal IRT1T2Loop T1T2Loop
		{
			get
			{
				Contract.Ensures(Contract.Result<IRT1T2Loop>() != null);

				return (IRT1T2Loop)this.m_rgn;
			}
		}
	}

	/// <summary>
	/// Keep track of the state of analyzing a T1T2Region
	/// </summary>
	internal sealed class T1T2BlockEvalState : T1T2RegionEvalState
	{
		/// <summary>
		/// The index of the block that we are currently analyzing.
		/// </summary>
		private int m_currentBlock;

		internal T1T2BlockEvalState(IRT1T2Block blck)
			: base(blck)
		{
			Contract.Requires(blck != null);
			this.m_currentBlock = 0; 
		}

		/// <summary>
		/// Get/Set the index of the sub T1T2Region that is being analyzed.
		/// </summary>
		internal int CurrentSubRegionIndex
		{
			get { return this.m_currentBlock; }
			set { this.m_currentBlock = value; }
		}

		/// <summary>
		/// Get the loop that this eval state relates to.
		/// </summary>
		internal IRT1T2Block T1T2Block
		{
			get
			{
				Contract.Ensures(Contract.Result<IRT1T2Block>() != null);

				return (IRT1T2Block)this.m_rgn;
			}
		}
	}

	/// <summary>
	/// Keep track of the state of analyzing a T1T2Region
	/// </summary>
	internal sealed class T1T2BasicBlockEvalState : T1T2RegionEvalState
	{
		/// <summary>
		/// The statement that is currently being analyzed.
		/// </summary>
		private int m_currentStmt;

		internal T1T2BasicBlockEvalState(IRBasicBlock blck)
			: base(blck)
		{
			Contract.Requires(blck != null);
			this.m_currentStmt = 0;
		}

		/// <summary>
		/// Get/Set the index of the statement that is being analyzed.
		/// </summary>
		internal int CurrentSubRegionIndex
		{
			get { return this.m_currentStmt; }
			set { this.m_currentStmt = value; }
		}

		/// <summary>
		/// Get the loop that this eval state relates to.
		/// </summary>
		internal IRBasicBlock BasicBlock
		{
			get
			{
				Contract.Ensures(Contract.Result<IRBasicBlock>() != null);

				return (IRBasicBlock)this.m_rgn;
			}
		}
	}
}
